\documentclass{beamer}
\graphicspath{{./figures/}}
\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}
\newcommand{\gsm}{\ensuremath{\mathcal{G}}~}
\newcommand{\sys}{\ensuremath{\mathcal{S}}~}

% \usepackage{beamerthemesplit} // Activate for custom appearance

\title{Combining Process and Ontological Modeling \\[12pt] Verification of Artifact-Centric Systems: Decidability and Modeling Issues}

\author{Dmitry Solomakhin \\ 
	{\small PhD student, XXVI cycle} \\\medskip
	{\small Supervisor: Prof. Sergio Tessaris}  \\ 
	{\small Co-supervisor: Prof. Marco Montali} \\
	{\small Co-supervisor: Prof. Diego Calvanese}}
\date{January 21, 2013}

\begin{document}

\frame{\titlepage}

\frame
{
	\frametitle{Outline}
	\tableofcontents
}

\section{Artifact-centric business modeling: a brush-up}
\frame
{
  \frametitle{Artifact-centric business modeling: a brush-up}
	\begin{itemize}
	\medskip
	\item \emph{Data-centric business modeling} = processes considered to be driven with the possible changes and evolutions of  \emph{artifacts}. 
	\medskip	\pause
	\item Guard-Stage-Milestone (GSM) - a declarative artifact modeling language, still lacks verification mechanisms. 
	\medskip \pause
	\item Evolution of data $\Rightarrow$ infinite-state systems $\Rightarrow$ verification of certain properties is \alert{undecidable}.
	\medskip \pause
	\item Data-centric dynamic systems (DCDSs) -- formal foundations of artifact-centric paradigm + some decidability results.
	\medskip \pause
	\item We aim at marrying the emerging modeling notation with the formal foundations of the data-centric paradigm.
	\end{itemize}
}

\section{Research questions: progress track}
\subsection{GSM formalization}
\frame{
  \frametitle{Progress track: GSM formalization}

	\textbf{\small Define a formal description of GSM methodology and its operational semantics (investigate different formalisms)}

	\begin{itemize}
		\item Data-Centric Dynamic Systems(DCDSs) -- a formal framework for the specification of data-aware business processes;
		\medskip \pause
		\item The translation relies on the GSM incremental semantics: \\a sequence of B-steps consisting of micro-steps;
		\item GSM micro-step $\equiv$ DCDS condition-action rule.
		\medskip \pause
		\item A sound and complete encoding of GSM into DCDSs.
		\medskip
		\item Allows to reproduce in the GSM context the decidability and complexity results recently established for DCDSs
	\end{itemize}
}

\subsection{Reasoning algorithms: dedicability and complexity}
\frame{
  \frametitle{Progress track: reasoning, decidability and complexity}
\textbf{\small Define the algorithms for the previously identified reasoning tasks and investigate the notions of complexity and decidability.} 
%
	\medskip
	\begin{itemize}
		\item \emph{State-bounded DCDSs} -- systems with bounded information model size at each possible moment along system execution.
		\medskip \pause
		\item Verification of certain properties over \emph{state-bounded DCDS} is decidable, and can be reduced to finite-state model checking of propositional $\mu$-calculus.
		\medskip \pause
		\item Given a GSM model \gsm and its DCDS translation \sys, \gsm is state-bounded if and only if \sys is state-bounded.
		\medskip
		\item Verification of certain properties over \textbf{Instance-bounded GSM models} is decidable.
		\medskip
		\item Inherited complexity boundaries: verification is \textsc{ExpTime} in the size of the GSM model.
	\end{itemize}
}

\subsection{Unifying modeling formalism for data and process}
\frame{
  \frametitle{Progress track: unifying modeling formalism}
	\textbf{\small Define a unifying formalism of modeling both processes and the data they depend on and manipulate.} 

	\begin{itemize}
		\item Natural and clear integration of 
			\begin{itemize}
				\item artifact-centric modeling -- for the process layer
				\item conceptual modeling -- for the data layer
			\end{itemize}
		\medskip \pause
		\item Guard-Stage-Milestone (GSM)
			\begin{itemize}
			\item focuses on a lifecycle, assuming informational model to be relational and predefined.
			\item uses OCL to define guards and milestone conditions.
			\end{itemize}
		\medskip \pause
		\only<3>{
		\item Business domain data may be of very complex structure
			\begin{itemize}
			\item requires special modeling instruments.
			\item subject to validation and verification of specific properties.
			\end{itemize}
		}
		\pause
		\item Object-Role Modeling (ORM)
			\begin{itemize}
			\item Graphical fact-oriented approach for modelling business domain information
			\item The core of the OMG standard SBVR, widely used.
			\item Formalizations in modal logics, description logics.
			\item Reasoning capabilities
			\end{itemize}
	\end{itemize}
}

\subsection{Modeling support for artifact-centric modeling}
\frame{
  \frametitle{Progress track: support for artifact-centric modeling}
	\textbf{\small Develop the instruments for modeling business process tightly coupled with underlying data by the means of conceptual methodologies.}

	\begin{itemize}
		\item Designing the information layer modeling the business domain
		\smallskip
		\begin{itemize}
			\item ORM2 Reasoning Support Add-in for NORMA modeling tool
			\medskip
			\item Allows for model verification and implicit inferences discovery
		\end{itemize} 
		\medskip \pause
		\item Artifact-centric system modeling support (to be developed)
		\smallskip
		\begin{itemize}
			\item Use ORM2 and/or description logics for guards and milestones
			\medskip
			\item Business process conformance and process validation
			\medskip
			\item Integration of the artifact modeling and reasoning support to the already exisiting prototype: Siena/Barcelona systems
		\end{itemize} 
	\end{itemize}
}

\subsection{Semantic layer of the ACSI paradigm}
\frame{
  \frametitle{Progress track: semantic layer of artifact abstract model}
	\textbf{\small Determine use cases for and benefits of the semantic layer in the ACSI Artifact paradigm.}\\
	\textbf{\small Attempt to define a ``GSM Semantic Model" as an implementation of the semantic layer of the ACSI Artifact Abstract Model.}
	
	\begin{itemize}
		\item Have not been investigated so far. 
		\medskip
		\item May become actual in the stage of modeling the information model of the artifact-centric system
		\medskip
		\item Using description logics for guards and milestones might involve ``semantic layer'' of GSM
	\end{itemize}
}

\section{Last year feedback analysis}
\frame{
  \frametitle{Last year feedback analysis}
	\textbf{\small  Understand which are the most important tasks and whether (and how) existing formalisms can be exploited in order to support the integration of process and data.}
	\medskip
	\begin{itemize}
		\item Modeling the business domain of a complex structure, validation of the model and verification of specific properties.  
		\medskip
		\item Artifact modeling and reasoning support: business process conformance and process validation.
	\end{itemize}
}

\frame{
  \frametitle{Last year feedback analysis}
	\textbf{\small  Focus the research by isolating a core set of important tasks and relate them with a concrete framework (e.g. GSM) and use cases.}
	\medskip
	\begin{itemize}
		\item Developed modeling guidelines can be employed to turn any GSM model into a state-bounded, verifiable model.
		\medskip
		\item Possible implementation of concrete GSM verifiers that can rely on standard finite-state model checkers.
		\medskip
		\item Collaboration with Laboratory of Applied Ontology (Nicola Guarino, Chiara Ghidini) in the area of conceptual modeling (ORM2) will supply necessary practical use cases and get valuable feedback on applicability of the research.

	\end{itemize}
}

\section{Further details on GSM formalization}
\frame{
  \frametitle{Further details on GSM formalization}
	\begin{figure}[h!]
		\centering
		\includegraphics[width=\textwidth]{ts}
	%\caption{Construction of the B-step transition system $\Upsilon_\gsm$ and unblocked-state transition system $\Upsilon_\sys$ for a GSM model \gsm with initial snapshot $s_0$ and the corresponding DCDS \sys}
	\label{fig:ts}
	\end{figure}
	\vspace*{-12pt}
	\begin{itemize}
		\item GSM micro-step $\equiv$ DCDS condition-action rule.
		\medskip
		\item A sound and complete encoding of GSM into DCDSs:
			\begin{itemize}
			\item Given a GSM model \gsm and its translation into a corresponding DCDS \sys, the corresponding B-step transition system $\Upsilon_\gsm$ and filtered unblocked-state transition system $\Upsilon_\sys|_\gsm$ are equivalent, i.e., $\Upsilon_\gsm \equiv \Upsilon_\sys|_\gsm$.
			\end{itemize}
	\end{itemize}
}

\section{Further details on state-bounded GSM models}
\frame{
  \frametitle{Further details on state-bounded GSM models}
	\begin{itemize}
		\item State-boundedness is a semantic condition, whose checking is \alert{undecidable} -- a syntactic condition for DCDSs is introduced. 
		\medskip \pause
		\only<2>{
			\item<alert@2> Not suitable for GSM-originated DCDSs.
			\medskip
			}
		\item The only source of state-unboundedness for GSM -- \emph{create-artifact-instance} service calls.
		\only<2>{
		\medskip
		\begin{figure}[t]
		\includegraphics[width=.9\textwidth]{unbounded-ts}
		%\caption{\label{fig:unbounded-ts} Unbounded execution of the GSM model in Fig.~\ref{fig:order-gsm}}
		\end{figure}
		}
		\medskip \pause
		\item Verification of certain properties over GSM models without \emph{create-artifact-instance} tasks is decidable.
		\medskip \pause
		\item \textbf{Instance-bounded GSM models} -- $N_{max}$ container-based artifact-creation semantics.
	\end{itemize}
}

\section{Future work}
\frame{
  \frametitle{Future work}
	\begin{itemize}
	\item Investigate natural and clear integration of GSM models with ORM2 models: related problems and disadvantages.
	\medskip
	\item Reassess decidability and complexity results in a setting where GSM relies on a rich knowledge base (an ontology) for its information model.
	\medskip
	\item Implement and integrate with Barcelona an artifact-centric system reasoning support tool: GSM verification engine.
	\medskip
	\item Collect use cases and justify obtained research results together with Laboratory of Applied Ontology.
	\end{itemize}
}

%\frame
%{
%  \frametitle{Motivation: Guard-state-milestone approach}
%	\begin{itemize}
%	\medskip
%	\item Guard-State-Milestone (GSM) - a declarative artifact modeling language, still lacks verification mechanisms. 
% Guard-State-Milestone (GSM) artifact modeling language supports the declarative specification of \emph{artifacts lifecycles},  used to specify acceptable evolutions of  business data. \vspace{4pt}
%	\medskip
%	\item We aim at marrying the emerging modeling notation with the formal foundations of the data-centric paradigm.
% In the current line of the research, we aim at marrying the emerging modeling notation for artifact-centric processes with the formal foundations of the data-centric paradigm.
%	\medskip
%	\item \emph{Short-term goals}: 
%		\begin{itemize}
%		\item formalize GSM as DCDS.
%		\item determine syntactic conditions over GSM that guarantee state-boundedness of corresponding DCDS. 
%		\end{itemize}
%	\medskip
%	\item Long-term goal: 
%		\begin{itemize}
%		\item Provide automated verification support during the design phase of 	a GSM process, assisting the modeler in checking certain properties of a model.
%		\end{itemize}
%	\end{itemize}
%}
\end{document}
